T:Type, as,bs,cs,ds:(T List).
(append(as; cs) = append(bs; ds)  (T List))
 ((||as|| = ||bs||  )  (||cs|| = ||ds||  ))
 guard(((as = bs)  (cs = ds))) 

latex

Definitions	t  T, s = t, x:AB(x), x:A. B(x), append(as; bs), type List, listp(A), cons(car; cdr), prop{i:l}, Type, ||as||, , #$n, n + m, left + right, P  Q, guard(T), x:A  B(x), P  Q, P  Q, void, [], False, ge(i; j), P  Q, P  Q, rec-case(a) of [] => s | x::y => z.t(x;y;z), f(a), x.A(x), Y, A  B, hd(l), {x:A| B(x)} , a < b, A, tl(l), True
Lemmas	iff wf, rev implies wf, ge wf, tl wf, hd wf, length append, add functionality wrt eq, non neg length, guard wf, length wf1, append wf